Lean勉強会 2023-12-17

Issueにenhancementとか色々書いている

L18-L26

code:memo

class IncidenceGeometry where

Point : Type u₁

Line : Type u₂

between : Point → Point → Point → Prop -- implies colinearity

onLine : Point → Line → Prop

ne_23_of_between : ∀ {a b c : Point}, between a b c → b ≠ c

line_unique_of_pts : ∀ {a b : Point}, ∀ {L M : Line}, a ≠ b → onLine a L → onLine b L → onLine a M → onLine b M → L = M

onLine_2_of_between : ∀ {a b c : Point}, ∀ {L : Line}, between a b c → onLine a L → onLine c L → onLine b L